perm filename BOYER.TIM[TIM,LSP]2 blob
sn#685283 filedate 1982-09-15 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00013 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 Comparison of LISPS
C00004 00003 The ELISP code
C00025 00004 (FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918
C00050 00005 The Maclisp Code
C00071 00006 The ELISP test
C00072 00007 Interlisp bcompl blocklib swap and noswap
C00075 00008 Interlisp bcompl no blocklib swap and noswap
C00079 00009 Maclisp
C00085 00010 Interlisp (Dolphin and Dorado)
C00116 00011 The INTERLISP VAX test
C00119 00012 SAIL
C00121 00013 SAIL (FIXSW T)
C00123 ENDMK
C⊗;
Comparison of LISPS
This page contains a summary. Subsequent pages contain the
code used and documentation of the tests. All the code was compiled.
Non GC time (seconds) GC time Total
MACLISP (2060) 8.5 5.3 13.8
UCILISP (2060, (nouuo nil)) 9.3 4.7 14
INTERLISP (bcompl, blklib, swap, 2060) 11 6 17
ELISP (2060) 11 7 18
INTERLISP (bcompl, blklib, noswap, 2060) 11 7.5 18.5
INTERLISP (Dorado, bcompl, blklib) 18 11 29
INTERLISP (bcompl, no blklib, noswap, 2060) 39 7 46
INTERLISP (bcompl, no blklib, swap, 2060) 64 6 70
INTERLISP (VAX-780) 80 3 83
ZETALISP (LM-2, 1meg, gc-on) breakdown not available 97
INTERLISP (Dolphin, 1meg, bcompl, blklib) 132 35 167
The ELISP code
(DECLARE (SPECIAL UNIFY-SUBST TEMP-TEMP))
(DE ADD-LEMMA (TERM)
(COND ((AND (NOT (ATOM TERM))
(EQ (CAR TERM)
(QUOTE EQUAL))
(NOT (ATOM (CADR TERM))))
(PUTPROP (CAR (CADR TERM))
(CONS TERM (GET (CAR (CADR TERM))
(QUOTE LEMMAS)))
(QUOTE LEMMAS)))
(T (ERROR (LIST (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM) TERM)
))))
(DE ADD-LEMMA-LST (LST)
(COND ((NULL LST)
T)
(T (ADD-LEMMA (CAR LST))
(ADD-LEMMA-LST (CDR LST)))))
(DE APPLY-SUBST (ALIST TERM)
(COND ((ATOM TERM)
(COND ((SETQ TEMP-TEMP (ASSOC TERM ALIST))
(CDR TEMP-TEMP))
(T TERM)))
(T (CONS (CAR TERM)
(APPLY-SUBST-LST ALIST (CDR TERM))))))
(DE APPLY-SUBST-LST (ALIST LST)
(COND ((NULL LST)
NIL)
(T (CONS (APPLY-SUBST ALIST (CAR LST))
(APPLY-SUBST-LST ALIST (CDR LST))))))
(DE FALSEP (X LST)
(OR (EQUAL X (QUOTE (F)))
(MEMBER X LST)))
(DE ONE-WAY-UNIFY (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
(ONE-WAY-UNIFY1 TERM1 TERM2)))
(DE ONE-WAY-UNIFY1 (TERM1 TERM2)
(COND ((ATOM TERM2)
(COND ((SETQ TEMP-TEMP (ASSOC TERM2 UNIFY-SUBST))
(EQUAL TERM1 (CDR TEMP-TEMP)))
(T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
UNIFY-SUBST))
T)))
((ATOM TERM1)
NIL)
((EQ (CAR TERM1)
(CAR TERM2))
(ONE-WAY-UNIFY1-LST (CDR TERM1)
(CDR TERM2)))
(T NIL)))
(DE ONE-WAY-UNIFY1-LST (LST1 LST2)
(COND ((NULL LST1)
T)
((ONE-WAY-UNIFY1 (CAR LST1)
(CAR LST2))
(ONE-WAY-UNIFY1-LST (CDR LST1)
(CDR LST2)))
(T NIL)))
(DE REWRITE (TERM)
(COND ((ATOM TERM)
TERM)
(T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
(REWRITE-ARGS (CDR TERM)))
(GET (CAR TERM)
(QUOTE LEMMAS))))))
(DE REWRITE-ARGS (LST)
(COND ((NULL LST)
NIL)
(T (CONS (REWRITE (CAR LST))
(REWRITE-ARGS (CDR LST))))))
(DE REWRITE-WITH-LEMMAS (TERM LST)
(COND ((NULL LST)
TERM)
((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
(T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))
(DE
SETUP NIL
(ADD-LEMMA-LST
(QUOTE ((EQUAL (COMPILE FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
(NIL))))
(EQUAL (EQP X Y)
(EQUAL (FIX X)
(FIX Y)))
(EQUAL (GREATERP X Y)
(LESSP Y X))
(EQUAL (LESSEQP X Y)
(NOT (LESSP Y X)))
(EQUAL (GREATEREQP X Y)
(NOT (LESSP X Y)))
(EQUAL (BOOLEAN X)
(OR (EQUAL X (T))
(EQUAL X (F))))
(EQUAL (IFF X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X)))
(EQUAL (EVEN1 X)
(IF (ZEROP X)
(T)
(ODD (SUB1 X))))
(EQUAL (COUNTPS- L PRED)
(COUNTPS-LOOP L PRED (ZERO)))
(EQUAL (FACT- I)
(FACT-LOOP I 1))
(EQUAL (REVERSE- X)
(REVERSE-LOOP X (NIL)))
(EQUAL (DIVIDES X Y)
(ZEROP (REMAINDER Y X)))
(EQUAL (ASSUME-TRUE VAR ALIST)
(CONS (CONS VAR (T))
ALIST))
(EQUAL (ASSUME-FALSE VAR ALIST)
(CONS (CONS VAR (F))
ALIST))
(EQUAL (TAUTOLOGY-CHECKER X)
(TAUTOLOGYP (NORMALIZE X)
(NIL)))
(EQUAL (FALSIFY X)
(FALSIFY1 (NORMALIZE X)
(NIL)))
(EQUAL (PRIME X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X (ADD1 (ZERO))))
(PRIME1 X (SUB1 X))))
(EQUAL (AND P Q)
(IF P (IF Q (T)
(F))
(F)))
(EQUAL (OR P Q)
(IF P (T)
(IF Q (T)
(F))
(F)))
(EQUAL (NOT P)
(IF P (F)
(T)))
(EQUAL (IMPLIES P Q)
(IF P (IF Q (T)
(F))
(T)))
(EQUAL (FIX X)
(IF (NUMBERP X)
X
(ZERO)))
(EQUAL (IF (IF A B C)
D E)
(IF A (IF B D E)
(IF C D E)))
(EQUAL (ZEROP X)
(OR (EQUAL X (ZERO))
(NOT (NUMBERP X))))
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))
(EQUAL (EQUAL (PLUS A B)
(ZERO))
(AND (ZEROP A)
(ZEROP B)))
(EQUAL (DIFFERENCE X X)
(ZERO))
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))
(EQUAL (EQUAL (ZERO)
(DIFFERENCE X Y))
(NOT (LESSP Y X)))
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X (ZERO))
(ZEROP Y))))
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))
(EQUAL (EQUAL (TIMES X Y)
(ZERO))
(OR (ZEROP X)
(ZEROP Y)))
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))
(EQUAL (NTH (ZERO)
I)
(ZERO))
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))
(EQUAL (EXP I (TIMES J K))
(EXP (EXP I J)
K))
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))
(EQUAL (REVERSE-LOOP X (NIL))
(REVERSE X))
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))
(EQUAL (REMAINDER Y 1)
(ZERO))
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X X)
(ZERO))
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
(ZERO)
BASE)
BASE)
(PLUS I J))
(EQUAL (GCD X Y)
(GCD Y X))
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))
(EQUAL (REMAINDER (TIMES X Z)
Z)
(ZERO))
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))
(EQUAL (EQUAL (FLATTEN X)
(CONS Y (NIL)))
(AND (NLISTP X)
(EQUAL X Y)))
(EQUAL (LISTP (GOPHER X))
(LISTP X))
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
(ZERO))
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X (ZERO))))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z (ZERO))
(EQUAL W 1))))
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X (ZERO))
(AND (NUMBERP X)
(EQUAL Y 1))))
(EQUAL (REMAINDER (TIMES Y X)
Y)
(ZERO))
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A (ZERO)))
(NOT (EQUAL B (ZERO)))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
(ZERO))
(EQUAL (SUB1 B)
(ZERO))))
(EQUAL (LESSP (LENGTH (DELETE X L))
(LENGTH L))
(MEMBER X L))
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))
(EQUAL (DSORT X)
(SORT2 X))
(EQUAL (LENGTH (CONS X1
(CONS X2
(CONS X3 (CONS X4
(CONS X5
(CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))
(EQUAL (SIGMA (ZERO)
I)
(QUOTIENT (TIMES I (ADD1 I))
2))
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))
(EQUAL (NTH (NIL)
I)
(IF (ZEROP I)
(NIL)
(ZERO)))
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
(ZERO)))
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS (ZERO)
(NIL))))
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
(ZERO)
(FIX X)))
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM)))))))
(DE TAUTOLOGYP (X TRUE-LST FALSE-LST)
(COND ((TRUEP X TRUE-LST)
T)
((FALSEP X FALSE-LST)
NIL)
((ATOM X)
NIL)
((EQ (CAR X)
(QUOTE IF))
(COND ((TRUEP (CADR X)
TRUE-LST)
(TAUTOLOGYP (CADDR X)
TRUE-LST FALSE-LST))
((FALSEP (CADR X)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST FALSE-LST))
(T (AND (TAUTOLOGYP (CADDR X)
(CONS (CADR X)
TRUE-LST)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST
(CONS (CADR X)
FALSE-LST))))))
(T NIL)))
(DE TAUTP (X)
(TAUTOLOGYP (REWRITE X)
NIL NIL))
(DE TEST NIL
(TIMER (TEST1)))
(DE TEST1 NIL
(PROG (TERM ANS)
(SETQ TERM
(APPLY-SUBST
(QUOTE ((X F (PLUS (PLUS A B)
(PLUS C (ZERO))))
(Y F (TIMES (TIMES A B)
(PLUS C D)))
(Z F (REVERSE (APPEND (APPEND A B)
(NIL))))
(U EQUAL (PLUS A B)
(DIFFERENCE X Y))
(W LESSP (REMAINDER A B)
(MEMBER A (LENGTH B)))))
(QUOTE (IMPLIES (AND (IMPLIES X Y)
(AND (IMPLIES Y Z)
(AND (IMPLIES Z U)
(IMPLIES U W))))
(IMPLIES X W)))))
(SETQ ANS (TAUTP TERM))
(RETURN (LIST ANS))))
(DE TRANS-OF-IMPLIES (N)
(LIST (QUOTE IMPLIES)
(TRANS-OF-IMPLIES1 N)
(LIST (QUOTE IMPLIES)
0 N)))
(DE TRANS-OF-IMPLIES1 (N)
(COND ((EQUAL N 1)
(LIST (QUOTE IMPLIES)
0 1))
(T (LIST (QUOTE AND)
(LIST (QUOTE IMPLIES)
(SUB1 N)
N)
(TRANS-OF-IMPLIES1 (SUB1 N))))))
(DE TRUEP (X LST)
(OR (EQUAL X (QUOTE (T)))
(MEMBER X LST)))
(FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918
changes to: IREWRITECOMS
previous date: " 5-Jul-82 12:11:22" <CL.BOYER.LISPS>IREWRITE..3)
(PRETTYCOMPRINT IREWRITECOMS)
(RPAQQ IREWRITECOMS ((FNS * IREWRITEFNS)
(PROP BLKLIBRARYDEF MEMBER)
(BLOCKS (REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST
APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY
ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME
REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS
SETUP TAUTOLOGYP TAUTP TEST
TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP
(ENTRIES TEST SETUP)
(BLKLIBRARY EQUAL MEMBER GETPROP)
(GLOBALVARS TEMP-TEMP UNIFY-SUBST)))))
(RPAQQ IREWRITEFNS (ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST
FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1
ONE-WAY-UNIFY1-LST PTIME REWRITE
REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP
TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES
TRANS-OF-IMPLIES1 TRUEP))
(DEFINEQ
(ADD-LEMMA
(LAMBDA (TERM)
(COND
((AND (NOT (ATOM TERM))
(EQ (CAR TERM)
(QUOTE EQUAL))
(NOT (ATOM (CADR TERM))))
(COND
((GETPROP (CAR (CADR TERM))
(QUOTE LEMMAS))
(PUTPROP (CAR (CADR TERM))
(QUOTE LEMMAS)
(CONS TERM (GETPROP (CAR (CADR TERM))
(QUOTE LEMMAS)))))
(T (SETPROPLIST (CAR (CADR TERM))
(CONS (QUOTE LEMMAS)
(CONS (LIST TERM)
(GETPROPLIST (CAR (CADR TERM))))))
)))
(T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM)
TERM)))))
(ADD-LEMMA-LST
(LAMBDA (LST)
(COND
((NULL LST)
T)
(T (ADD-LEMMA (CAR LST))
(ADD-LEMMA-LST (CDR LST))))))
(APPLY-SUBST
(LAMBDA (ALIST TERM)
(COND
((NLISTP TERM)
(COND
((SETQ TEMP-TEMP (FASSOC TERM ALIST))
(CDR TEMP-TEMP))
(T TERM)))
(T (CONS (CAR TERM)
(APPLY-SUBST-LST ALIST (CDR TERM)))))))
(APPLY-SUBST-LST
(LAMBDA (ALIST LST)
(COND
((NULL LST)
NIL)
(T (CONS (APPLY-SUBST ALIST (CAR LST))
(APPLY-SUBST-LST ALIST (CDR LST)))))))
(FALSEP
(LAMBDA (X LST)
(OR (EQUAL X (QUOTE (F)))
(MEMBER X LST))))
(ONE-WAY-UNIFY
(LAMBDA (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
(ONE-WAY-UNIFY1 TERM1 TERM2))))
(ONE-WAY-UNIFY1
(LAMBDA (TERM1 TERM2)
(COND
((NLISTP TERM2)
(COND
((SETQ TEMP-TEMP (FASSOC TERM2 UNIFY-SUBST))
(EQUAL TERM1 (CDR TEMP-TEMP)))
(T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
UNIFY-SUBST))
T)))
((ATOM TERM1)
NIL)
((EQ (CAR TERM1)
(CAR TERM2))
(ONE-WAY-UNIFY1-LST (CDR TERM1)
(CDR TERM2)))
(T NIL))))
(ONE-WAY-UNIFY1-LST
(LAMBDA (LST1 LST2)
(COND
((NULL LST1)
T)
((ONE-WAY-UNIFY1 (CAR LST1)
(CAR LST2))
(ONE-WAY-UNIFY1-LST (CDR LST1)
(CDR LST2)))
(T NIL))))
(PTIME
(LAMBDA NIL
(PROG (GCTM)
(SETQ GCTM (CLOCK 3))
(RETURN (CONS (IPLUS (CLOCK 2)
GCTM)
GCTM)))))
(REWRITE
(LAMBDA (TERM)
(COND
((NLISTP TERM)
TERM)
(T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
(REWRITE-ARGS (CDR TERM)))
(GETPROP (CAR TERM)
(QUOTE LEMMAS)))))))
(REWRITE-ARGS
(LAMBDA (LST)
(COND
((NULL LST)
NIL)
(T (CONS (REWRITE (CAR LST))
(REWRITE-ARGS (CDR LST)))))))
(REWRITE-WITH-LEMMAS
(LAMBDA (TERM LST)
(COND
((NULL LST)
TERM)
((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
(T (REWRITE-WITH-LEMMAS TERM (CDR LST))))))
(SETUP
(LAMBDA NIL
(ADD-LEMMA-LST
(QUOTE
((EQUAL (COMPILE FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
(NIL))))
(EQUAL (EQP X Y)
(EQUAL (FIX X)
(FIX Y)))
(EQUAL (GREATERP X Y)
(LESSP Y X))
(EQUAL (LESSEQP X Y)
(NOT (LESSP Y X)))
(EQUAL (GREATEREQP X Y)
(NOT (LESSP X Y)))
(EQUAL (BOOLEAN X)
(OR (EQUAL X (T))
(EQUAL X (F))))
(EQUAL (IFF X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X)))
(EQUAL (EVEN1 X)
(IF (ZEROP X)
(T)
(ODD (SUB1 X))))
(EQUAL (COUNTPS- L PRED)
(COUNTPS-LOOP L PRED (ZERO)))
(EQUAL (FACT- I)
(FACT-LOOP I 1))
(EQUAL (REVERSE- X)
(REVERSE-LOOP X (NIL)))
(EQUAL (DIVIDES X Y)
(ZEROP (REMAINDER Y X)))
(EQUAL (ASSUME-TRUE VAR ALIST)
(CONS (CONS VAR (T))
ALIST))
(EQUAL (ASSUME-FALSE VAR ALIST)
(CONS (CONS VAR (F))
ALIST))
(EQUAL (TAUTOLOGY-CHECKER X)
(TAUTOLOGYP (NORMALIZE X)
(NIL)))
(EQUAL (FALSIFY X)
(FALSIFY1 (NORMALIZE X)
(NIL)))
(EQUAL (PRIME X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X (ADD1 (ZERO))))
(PRIME1 X (SUB1 X))))
(EQUAL (AND P Q)
(IF P (IF Q (T)
(F))
(F)))
(EQUAL (OR P Q)
(IF P (T)
(IF Q (T)
(F))
(F)))
(EQUAL (NOT P)
(IF P (F)
(T)))
(EQUAL (IMPLIES P Q)
(IF P (IF Q (T)
(F))
(T)))
(EQUAL (FIX X)
(IF (NUMBERP X)
X
(ZERO)))
(EQUAL (IF (IF A B C)
D E)
(IF A (IF B D E)
(IF C D E)))
(EQUAL (ZEROP X)
(OR (EQUAL X (ZERO))
(NOT (NUMBERP X))))
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))
(EQUAL (EQUAL (PLUS A B)
(ZERO))
(AND (ZEROP A)
(ZEROP B)))
(EQUAL (DIFFERENCE X X)
(ZERO))
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))
(EQUAL (EQUAL (ZERO)
(DIFFERENCE X Y))
(NOT (LESSP Y X)))
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X (ZERO))
(ZEROP Y))))
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))
(EQUAL (EQUAL (TIMES X Y)
(ZERO))
(OR (ZEROP X)
(ZEROP Y)))
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))
(EQUAL (NTH (ZERO)
I)
(ZERO))
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))
(EQUAL (EXP I (TIMES J K))
(EXP (EXP I J)
K))
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))
(EQUAL (REVERSE-LOOP X (NIL))
(REVERSE X))
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))
(EQUAL (REMAINDER Y 1)
(ZERO))
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X X)
(ZERO))
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
(ZERO)
BASE)
BASE)
(PLUS I J))
(EQUAL (GCD X Y)
(GCD Y X))
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))
(EQUAL (REMAINDER (TIMES X Z)
Z)
(ZERO))
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))
(EQUAL (EQUAL (FLATTEN X)
(CONS Y (NIL)))
(AND (NLISTP X)
(EQUAL X Y)))
(EQUAL (LISTP (GOPHER X))
(LISTP X))
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))
(EQUAL (EQUAL (GREATEST-FACTOR X Y(π~ (ZERO))
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X (ZERO))))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z (ZERO))
(EQUAL W 1))))
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X (ZERO))
(AND (NUMBERP X)
(EQUAL Y 1))))
(EQUAL (REMAINDER (TIMES Y X)
Y)
(ZERO))
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A (ZERO)))
(NOT (EQUAL B (ZERO)))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
(ZERO))
(EQUAL (SUB1 B)
(ZERO))))
(EQUAL (LESSP (LENGTH (DELETE X L))
(LENGTH L))
(MEMBER X L))
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))
(EQUAL (DSORT X)
(SORT2 X))
(EQUAL
(LENGTH (CONS X1
(CONS X2
(CONS X3
(CONS X4 (CONS X5
(CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))
(EQUAL (SIGMA (ZERO)
I)
(QUOTIENT (TIMES I (ADD1 I))
2))
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))
(EQUAL (NTH (NIL)
I)
(IF (ZEROP I)
(NIL)
(ZERO)))
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
(ZERO)))
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS (ZERO)
(NIL))))
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
(ZERO)
(FIX X)))
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM))))))))
(TAUTOLOGYP
(LAMBDA (X TRUE-LST FALSE-LST)
(COND
((TRUEP X TRUE-LST)
T)
((FALSEP X FALSE-LST)
NIL)
((NLISTP X)
NIL)
((EQ (CAR X)
(QUOTE IF))
(COND
((TRUEP (CADR X)
TRUE-LST)
(TAUTOLOGYP (CADDR X)
TRUE-LST FALSE-LST))
((FALSEP (CADR X)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST FALSE-LST))
(T (AND (TAUTOLOGYP (CADDR X)
(CONS (CADR X)
TRUE-LST)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST
(CONS (CADR X)
FALSE-LST))))))
(T NIL))))
(TAUTP
(LAMBDA (X)
(TAUTOLOGYP (REWRITE X)
NIL NIL)))
(TEST
(LAMBDA NIL
(PROG (TM1 TM2 ANS TERM)
(SETQ TM1 (PTIME))
(SETQ TERM
(APPLY-SUBST
(QUOTE ((X F (PLUS (PLUS A B)
(PLUS C (ZERO))))
(Y F (TIMES (TIMES A B)
(PLUS C D)))
(Z F (REVERSE (APPEND (APPEND A B)
(NIL))))
(U EQUAL (PLUS A B)
(DIFFERENCE X Y))
(W LESSP (REMAINDER A B)
(MEMBER A (LENGTH B)))))
(QUOTE (IMPLIES (AND (IMPLIES X Y)
(AND (IMPLIES Y Z)
(AND (IMPLIES Z U)
(IMPLIES U W))))
(IMPLIES X W)))))
(SETQ ANS (TAUTP TERM))
(SETQ TM2 (PTIME))
(RETURN (LIST ANS (DIFFERENCE (CAR TM2)
(CAR TM1))
(DIFFERENCE (CDR TM2)
(CDR TM1)))))))
(TRANS-OF-IMPLIES
(LAMBDA (N)
(LIST (QUOTE IMPLIES)
(TRANS-OF-IMPLIES1 N)
(LIST (QUOTE IMPLIES)
0 N))))
(TRANS-OF-IMPLIES1
(LAMBDA (N)
(COND
((EQUAL N 1)
(LIST (QUOTE IMPLIES)
0 1))
(T (LIST (QUOTE AND)
(LIST (QUOTE IMPLIES)
(SUB1 N)
N)
(TRANS-OF-IMPLIES1 (SUB1 N)))))))
(TRUEP
(LAMBDA (X LST)
(OR (EQUAL X (QUOTE (T)))
(MEMBER X LST))))
)
(PUTPROPS MEMBER BLKLIBRARYDEF (LAMBDA
(.BLKVAR.X .BLKVAR.Y)
(DECLARE (LOCALVARS . T))
(PROG NIL LP (RETURN (COND ((NLISTP .BLKVAR.Y)
NIL)
((EQUAL .BLKVAR.X (CAR .BLKVAR.Y)
)
.BLKVAR.Y)
(T (SETQ .BLKVAR.Y (CDR
.BLKVAR.Y))
(GO LP)))))))
[DECLARE: DONTEVAL@LOAD DOEVAL@COMPILE DONTCOPY
(BLOCK: REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST
APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1
ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS
REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST
TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES TEST SETUP)
(BLKLIBRARY EQUAL MEMBER GETPROP)
(GLOBALVARS TEMP-TEMP UNIFY-SUBST))
]
(DECLARE: DONTCOPY
(FILEMAP (NIL (1018 14165 (ADD-LEMMA 1030 . 1573) (ADD-LEMMA-LST 1577 .
1708) (APPLY-SUBST 1712 . 1945) (APPLY-SUBST-LST 1949 . 2119) (FALSEP
2123 . 2200) (ONE-WAY-UNIFY 2204 . 2315) (ONE-WAY-UNIFY1 2319 . 2717) (
ONE-WAY-UNIFY1-LST 2721 . 2928) (PTIME 2932 . 3077) (REWRITE 3081 . 3295
) (REWRITE-ARGS 3299 . 3441) (REWRITE-WITH-LEMMAS 3445 . 3679) (SETUP
3683 . 12295) (TAUTOLOGYP 12299 . 12890) (TAUTP 12894 . 12958) (TEST
12962 . 13720) (TRANS-OF-IMPLIES 13724 . 13846) (TRANS-OF-IMPLIES1 13850
. 14082) (TRUEP 14086 . 14162)))))
STOP
The Maclisp Code
(DECLARE (SPECIAL UNIFY-SUBST TEMP-TEMP))
(DEFUN PTIME NIL (LIST (RUNTIME) (STATUS GCTIME)))
(DEFUN ADD-LEMMA (TERM)
(COND ((AND (NOT (ATOM TERM))
(EQ (CAR TERM)
(QUOTE EQUAL))
(NOT (ATOM (CADR TERM))))
(PUTPROP (CAR (CADR TERM))
(CONS TERM (GET (CAR (CADR TERM))
(QUOTE LEMMAS)))
(QUOTE LEMMAS)))
(T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM)
TERM))))
(DEFUN ADD-LEMMA-LST (LST)
(COND ((NULL LST)
T)
(T (ADD-LEMMA (CAR LST))
(ADD-LEMMA-LST (CDR LST)))))
(DEFUN APPLY-SUBST (ALIST TERM)
(COND ((ATOM TERM)
(COND ((SETQ TEMP-TEMP (ASSQ TERM ALIST))
(CDR TEMP-TEMP))
(T TERM)))
(T (CONS (CAR TERM)
(APPLY-SUBST-LST ALIST (CDR TERM))))))
(DEFUN APPLY-SUBST-LST (ALIST LST)
(COND ((NULL LST)
NIL)
(T (CONS (APPLY-SUBST ALIST (CAR LST))
(APPLY-SUBST-LST ALIST (CDR LST))))))
(DEFUN FALSEP (X LST)
(OR (EQUAL X (QUOTE (F)))
(MEMBER X LST)))
(DEFUN ONE-WAY-UNIFY (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
(ONE-WAY-UNIFY1 TERM1 TERM2)))
(DEFUN ONE-WAY-UNIFY1 (TERM1 TERM2)
(COND ((ATOM TERM2)
(COND ((SETQ TEMP-TEMP (ASSQ TERM2 UNIFY-SUBST))
(EQUAL TERM1 (CDR TEMP-TEMP)))
(T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
UNIFY-SUBST))
T)))
((ATOM TERM1)
NIL)
((EQ (CAR TERM1)
(CAR TERM2))
(ONE-WAY-UNIFY1-LST (CDR TERM1)
(CDR TERM2)))
(T NIL)))
(DEFUN ONE-WAY-UNIFY1-LST (LST1 LST2)
(COND ((NULL LST1)
T)
((ONE-WAY-UNIFY1 (CAR LST1)
(CAR LST2))
(ONE-WAY-UNIFY1-LST (CDR LST1)
(CDR LST2)))
(T NIL)))
(DEFUN REWRITE (TERM)
(COND ((ATOM TERM)
TERM)
(T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
(REWRITE-ARGS (CDR TERM)))
(GET (CAR TERM)
(QUOTE LEMMAS))))))
(DEFUN REWRITE-ARGS (LST)
(COND ((NULL LST)
NIL)
(T (CONS (REWRITE (CAR LST))
(REWRITE-ARGS (CDR LST))))))
(DEFUN REWRITE-WITH-LEMMAS (TERM LST)
(COND ((NULL LST)
TERM)
((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
(T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))
(DEFUN
SETUP NIL
(ADD-LEMMA-LST
(QUOTE ((EQUAL (COMPILE FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
(NIL))))
(EQUAL (EQP X Y)
(EQUAL (FIX X)
(FIX Y)))
(EQUAL (GREATERP X Y)
(LESSP Y X))
(EQUAL (LESSEQP X Y)
(NOT (LESSP Y X)))
(EQUAL (GREATEREQP X Y)
(NOT (LESSP X Y)))
(EQUAL (BOOLEAN X)
(OR (EQUAL X (T))
(EQUAL X (F))))
(EQUAL (IFF X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X)))
(EQUAL (EVEN1 X)
(IF (ZEROP X)
(T)
(ODD (SUB1 X))))
(EQUAL (COUNTPS- L PRED)
(COUNTPS-LOOP L PRED (ZERO)))
(EQUAL (FACT- I)
(FACT-LOOP I 1))
(EQUAL (REVERSE- X)
(REVERSE-LOOP X (NIL)))
(EQUAL (DIVIDES X Y)
(ZEROP (REMAINDER Y X)))
(EQUAL (ASSUME-TRUE VAR ALIST)
(CONS (CONS VAR (T))
ALIST))
(EQUAL (ASSUME-FALSE VAR ALIST)
(CONS (CONS VAR (F))
ALIST))
(EQUAL (TAUTOLOGY-CHECKER X)
(TAUTOLOGYP (NORMALIZE X)
(NIL)))
(EQUAL (FALSIFY X)
(FALSIFY1 (NORMALIZE X)
(NIL)))
(EQUAL (PRIME X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X (ADD1 (ZERO))))
(PRIME1 X (SUB1 X))))
(EQUAL (AND P Q)
(IF P (IF Q (T)
(F))
(F)))
(EQUAL (OR P Q)
(IF P (T)
(IF Q (T)
(F))
(F)))
(EQUAL (NOT P)
(IF P (F)
(T)))
(EQUAL (IMPLIES P Q)
(IF P (IF Q (T)
(F))
(T)))
(EQUAL (FIX X)
(IF (NUMBERP X)
X
(ZERO)))
(EQUAL (IF (IF A B C)
D E)
(IF A (IF B D E)
(IF C D E)))
(EQUAL (ZEROP X)
(OR (EQUAL X (ZERO))
(NOT (NUMBERP X))))
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))
(EQUAL (EQUAL (PLUS A B)
(ZERO))
(AND (ZEROP A)
(ZEROP B)))
(EQUAL (DIFFERENCE X X)
(ZERO))
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))
(EQUAL (EQUAL (ZERO)
(DIFFERENCE X Y))
(NOT (LESSP Y X)))
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X (ZERO))
(ZEROP Y))))
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))
(EQUAL (EQUAL (TIMES X Y)
(ZERO))
(OR (ZEROP X)
(ZEROP Y)))
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))
(EQUAL (NTH (ZERO)
I)
(ZERO))
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))
(EQUAL (EXP I (TIMES J K))
(EXP (EXP I J)
K))
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))
(EQUAL (REVERSE-LOOP X (NIL))
(REVERSE X))
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))
(EQUAL (REMAINDER Y 1)
(ZERO))
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X X)
(ZERO))
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
(ZERO)
BASE)
BASE)
(PLUS I J))
(EQUAL (GCD X Y)
(GCD Y X))
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))
(EQUAL (REMAINDER (TIMES X Z)
Z)
(ZERO))
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))
(EQUAL (EQUAL (FLATTEN X)
(CONS Y (NIL)))
(AND (NLISTP X)
(EQUAL X Y)))
(EQUAL (LISTP (GOPHER X))
(LISTP X))
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
(ZERO))
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X (ZERO))))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z (ZERO))
(EQUAL W 1))))
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X (ZERO))
(AND (NUMBERP X)
(EQUAL Y 1))))
(EQUAL (REMAINDER (TIMES Y X)
Y)
(ZERO))
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A (ZERO)))
(NOT (EQUAL B (ZERO)))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
(ZERO))
(EQUAL (SUB1 B)
(ZERO))))
(EQUAL (LESSP (LENGTH (DELETE X L))
(LENGTH L))
(MEMBER X L))
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))
(EQUAL (DSORT X)
(SORT2 X))
(EQUAL (LENGTH (CONS X1
(CONS X2
(CONS X3 (CONS X4
(CONS X5
(CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))
(EQUAL (SIGMA (ZERO)
I)
(QUOTIENT (TIMES I (ADD1 I))
2))
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))
(EQUAL (NTH (NIL)
I)
(IF (ZEROP I)
(NIL)
(ZERO)))
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
(ZERO)))
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS (ZERO)
(NIL))))
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
(ZERO)
(FIX X)))
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM)))))))
(DEFUN TAUTOLOGYP (X TRUE-LST FALSE-LST)
(COND ((TRUEP X TRUE-LST)
T)
((FALSEP X FALSE-LST)
NIL)
((ATOM X)
NIL)
((EQ (CAR X)
(QUOTE IF))
(COND ((TRUEP (CADR X)
TRUE-LST)
(TAUTOLOGYP (CADDR X)
TRUE-LST FALSE-LST))
((FALSEP (CADR X)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST FALSE-LST))
(T (AND (TAUTOLOGYP (CADDR X)
(CONS (CADR X)
TRUE-LST)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST
(CONS (CADR X)
FALSE-LST))))))
(T NIL)))
(DEFUN TAUTP (X)
(TAUTOLOGYP (REWRITE X)
NIL NIL))
(DEFUN TEST NIL
(PROG (TM1 TM2 ANS TERM)
(SETQ TM1 (PTIME))
(SETQ TERM
(APPLY-SUBST
(QUOTE ((X F (PLUS (PLUS A B)
(PLUS C (ZERO))))
(Y F (TIMES (TIMES A B)
(PLUS C D)))
(Z F (REVERSE (APPEND (APPEND A B)
(NIL))))
(U EQUAL (PLUS A B)
(DIFFERENCE X Y))
(W LESSP (REMAINDER A B)
(MEMBER A (LENGTH B)))))
(QUOTE (IMPLIES (AND (IMPLIES X Y)
(AND (IMPLIES Y Z)
(AND (IMPLIES Z U)
(IMPLIES U W))))
(IMPLIES X W)))))
(SETQ ANS (TAUTP TERM))
(SETQ TM2 (PTIME))
(RETURN (LIST ANS (DIFFERENCE (CAR TM2)
(CAR TM1))
(DIFFERENCE (CADR TM2)
(CADR TM1))))))
(DEFUN TRANS-OF-IMPLIES (N)
(LIST (QUOTE IMPLIES)
(TRANS-OF-IMPLIES1 N)
(LIST (QUOTE IMPLIES)
0 N)))
(DEFUN TRANS-OF-IMPLIES1 (N)
(COND ((EQUAL N 1)
(LIST (QUOTE IMPLIES)
0 1))
(T (LIST (QUOTE AND)
(LIST (QUOTE IMPLIES)
(SUB1 N)
N)
(TRANS-OF-IMPLIES1 (SUB1 N))))))
(DEFUN TRUEP (X LST)
(OR (EQUAL X (QUOTE (T)))
(MEMBER X LST)))
The ELISP test
[PHOTO: Recording initiated Tue 29-Jun-82 12:23PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4A(67)-1
End of <CL.BOYER>COMAND.CMD.1
@<ELISP>ELISP
[Keeping]
Elisp, 4 27 82
*(DSKIN "EREWRITE.FLAP")
"EREWRITE.FLAP.2"
Files-Loaded
*(SETUP)
T
*(TEST)
19776 msec CPU (7447 msec GC), 41583 msec clock, 452930 words consed
(T)
*(TEST)
18185 msec CPU (6361 msec GC), 51621 msec clock, 452930 words consed
(T)
*↑C
@POP
[PHOTO: Recording terminated Tue 29-Jun-82 12:26PM]
Interlisp bcompl blocklib swap and noswap
[PHOTO: Recording initiated Mon 5-Jul-82 12:16PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4B(70)-1
End of <CL.BOYER>COMAND.CMD.1
@LISP.EXE.133
INTERLISP-10 27-NOV-79 ...
collecting lists
716, 10444 free cells
control-A is an interrupt and can't be an edit control-character
Good afternoon, Bob.
2←LOAD(IREWRITE.COM]
compiled on 5-Jul-82 12:11:29
FILE CREATED 5-Jul-82 12:11:22
IREWRITECOMS
<CL.BOYER.LISPS>IREWRITE.COM.3
3←IREWRITECOMS
((FNS * IREWRITEFNS) (PROP BLKLIBRARYDEF MEMBER SASSOC) (BLOCKS (REWRITEBLOCK
ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY
ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS
SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES
TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST)
)))
4←NOSWAPFLG
NIL
5←(MINFS 100000]
10000
6←(RECLAIM]
collecting lists
7245, 92749 free cells, 0 pages left
92749
7←(GCGAG]
40
8←(MINFS 10000]
100000
9←SETUP]
T
10←(TEST]
(T 15821 4995)
11←(TEST]
(T 17498 6245)
12←(TEST]
(T 16569 5954)
13←(TEST]
(T 16707 5925)
14←(SETQ NOSWAPFLG T]
(NOSWAPFLG reset)
T
15←LOAD(IREWRITE.COM]
compiled on 5-Jul-82 12:11:29
FILE CREATED 5-Jul-82 12:11:22
(REWRITEBLOCK redefined)
(TEST redefined)
(SETUP redefined)
IREWRITECOMS
<CL.BOYER.LISPS>IREWRITE.COM.3
16←TEST]
(T 19546 8561)
17←TEST]
(T 17431 6601)
18←TEST]
(T 17192 6511)
19←TEST]
(T 18785 8161)
20←↑C
@POP
[PHOTO: Recording terminated Mon 5-Jul-82 12:29PM]
Interlisp bcompl no blocklib swap and noswap
[PHOTO: Recording initiated Mon 5-Jul-82 12:29PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4B(70)-1
End of <CL.BOYER>COMAND.CMD.1
@LISP.EXE.133
INTERLISP-10 27-NOV-79 ...
collecting lists
716, 10444 free cells
control-A is an interrupt and can't be an edit control-character
Hello, Bob.
2←LOAD(IREWRITE]
FILE CREATED 5-Jul-82 12:11:22
IREWRITECOMS
<CL.BOYER.LISPS>IREWRITE..3
3←IREWRITECOMS
((FNS * IREWRITEFNS) (PROP BLKLIBRARYDEF MEMBER SASSOC) (BLOCKS (REWRITEBLOCK
ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY
ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS
SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES
TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST)
)))
4←(BLOCKCOMPILE 'REWRITEBLOCK IREWRITEFNS '(TEST SETUP]
listing? STore and redefine
output file? No
(REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP
ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS
REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES
TRANS-OF-IMPLIES1 TRUEP)
(REWRITEBLOCK (REWRITEBLOCK#0) (TEMP-TEMP UNIFY-SUBST))
collecting lists
6001, 10097 free cells
(TEST NIL NIL)
(TEST redefined)
(SETUP NIL NIL)
(SETUP redefined)
(TEST SETUP)
5←(SETUP]
T
6←(MINFS 100000]
10000
7←(RECLAIM]
collecting lists
9850, 90234 free cells, 0 pages left
90234
8←(MINFS 10000]
100000
9←(GCGAG]
40
10←NOSWAPFLG
NIL
11←(TEST]
(T 31978 6737)
12←(TEST]
(T 47072 6180)
13←(TEST]
LISP Running at 30547 Used 0:10:10.7 in 2:40:39, Load 3.06
(T 71046 6316)
14←(TEST]
LISP Running at 30525 Used 0:11:45.7 in 2:44:33, Load 2.85
(T 71222 7772)
15←(TEST]
(T 70026 6175)
16←(SETQ NOSWAPFLG T]
(NOSWAPFLG reset)
T
17←REDO BLOCKCOMPILE
listing? ST
output file? N
(REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP
ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS
REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES
TRANS-OF-IMPLIES1 TRUEP)
(REWRITEBLOCK (REWRITEBLOCK#0) (TEMP-TEMP UNIFY-SUBST))
(REWRITEBLOCK redefined)
(TEST NIL NIL)
(TEST redefined)
(SETUP NIL NIL)
(SETUP redefined)
(TEST SETUP)
18←(TEST]
(T 46501 7685)
19←TEST]
(T 45285 6068)
20←TEST]
(T 46995 7564)
21←TEST]
(T 46522 6180)
22←↑C
@POP
[PHOTO: Recording terminated Mon 5-Jul-82 12:51PM]
Maclisp
[PHOTO: Recording initiated Tue 29-Jun-82 12:26PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4A(67)-1
End of <CL.BOYER>COMAND.CMD.1
@<ATP.MURRAY>MACLSP
LISP 1983
Alloc? Y
# REGPDL = 4000
# SPECPDL = 2000
# FXPDL = 4000
# FLPDL = 1000
LIST = 40000 100000.
SYMBOL = 6000 $
*
(SETQ BASE (SETQ IBASE 10.))
10.
(FASLOAD MREWRITE)
40307.
(SETUP)
T
(TEST)
(T 20190000. 11905000.)
(TEST)
(T 13728000. 5236000.)
(TEST)
(T 13708000. 5398000.)
↑C
@POP
[PHOTO: Recording terminated Tue 29-Jun-82 12:29PM]
**********************************************************************
UCILISP
[PHOTO: Recording initiated Wed 30-Jun-82 12:16PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4B(70)-1
End of <CL.BOYER>COMAND.CMD.1
@
@ucilsp
UT/UCI LISP - 8/10/80
*(gcgag t)
NIL
*(gc)
3790 FREE STG, 1129 FULL WORDS AVAILABLE
NIL
*(expfs 100000.)
FREE STG EXHAUSTED
FULL WORD SPACE EXHAUSTED
101112 FREE STG, 1131 FULL WORDS AVAILABLE
*(loa≠≠≠≠Jdskin (rewrit.lap))
(ADD-LEMMA 32) (ADD-LEMMA-LST 10) (APPLY-SUBST 23) (APPLY-SUBST-LST 15)
(FALSEP 10) (ONE-WAY-UNIFY 2)
Binary Program Space exceeded
*(expbps 1000)
FREE STG EXHAUSTED
FULL WORD SPACE EXHAUSTED
101012 FREE STG, 1091 FULL WORDS AVAILABLE
*(dskin (rewrit.lap))
(ADD-LEMMA 32) (ADD-LEMMA-LST 10) (APPLY-SUBST 23) (APPLY-SUBST-LST 15)
(FALSEP 10) (ONE-WAY-UNIFY 2) (ONE-WAY-UNIFY1 38) (ONE-WAY-UNIFY1-LST 15)
(REWRITE 20) (REWRITE-ARGS 11) (REWRITE-WITH-LEMMAS 22) (SETUP 2) (TAUTOLOGYP
66) (TAUTP 4) (TEST 2) (TEST1 8) (TRANS-OF-IMPLIES 13) (TRANS-OF-IMPLIES1 31)
(TRUEP 10)
FILES-LOADED
*(setup)
T
*(test)
FREE STG EXHAUSTED
63969 FREE STG, 943 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
47018 FREE STG, 943 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
40438 FREE STG, 943 FULL WORDS AVAILABLE
50614 msec CPU (3738 msec GC), 67496 msec clock, 226465 conses
(T)
*(test)
FREE STG EXHAUSTED
94012 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
58810 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
47089 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
35091 FREE STG, 942 FULL WORDS AVAILABLE
51676 msec CPU (4605 msec GC), 72196 msec clock, 226467 conses
(T)
*(test)
FREE STG EXHAUSTED
91609 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
57005 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
45700 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
34252 FREE STG, 942 FULL WORDS AVAILABLE
52328 msec CPU (4809 msec GC), 70687 msec clock, 226467 conses
(T)
*(nouuo nil)
T
*(test)
FREE STG EXHAUSTED
89843 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
56841 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
45727 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
34117 FREE STG, 942 FULL WORDS AVAILABLE
14099 msec CPU (4711 msec GC), 20077 msec clock, 226467 conses
(T)
*(test)
FREE STG EXHAUSTED
89806 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
56830 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
45727 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
34117 FREE STG, 942 FULL WORDS AVAILABLE
13827 msec CPU (4712 msec GC), 19857 msec clock, 226467 conses
(T)
*
@pop
[PHOTO: Recording terminated Wed 30-Jun-82 12:24PM]
Interlisp (Dolphin and Dorado)
Date: 8 Jul 1982 18:56 PDT
From: JonL at PARC-MAXC
Reply-To: JonL at PARC-MAXC
To: NOVAK at SUMEX-AIM
cc: CL.BOYER, Masinter at PARC-MAXC, LispCore↑ at PARC-MAXC
Re: The Boyer-Moore-Novak Benchmarkings
Gordon, I'll have to apologize for waiting so long to get you the results
of the timing comparisons between your machine and the various
configurations at PARC. I was "laid-low" last Saturday with either a
summer flu, or a severe allergic reaction (hay fever), and couldn't get
the results summarized until yesterday.
I have six areas that I want to summarize in this note:
Translation Inadequacy due to the FreeVars Trip-Up
"Ineffable" Factors Tending to make timing runs Un-Reproducible
PUP Activity -- Ephemeral as well as Ineffable
What the Faster Clock on buys
What DISPLAYDOWN buys
What you can Expect for Dolphin Speed Increases Soon
Briefly, the "FreeVars Trip-Up" and the DISPLAYDOWN account
for most of the sluggishness of the timings you made, but also there's
one "ineffable" which might be sabotaging you.
Below these sections, I've tried to display my data in good scientific
fashion; you'll note that I give a "First run" time and a "Mode run" time.
What this means is the "First run" must absorb all the "ineffable" costs of
swapping in the necessary code and data parts, and of initially-building
the List-space pages that will be used and re-used on subsequent runs.
Also included are one set of timings from a Dorado, just for comparison.
Generally, my comparisons will be of "speed" rather than "time". Thus
if one trial takes 40 secs, and another takes 50 secs, then the first one
runs 25% faster (the other way of saying it would be that the first one
takes 20% less time). The rationale is this: the first one "computes"
.025 MegaFrumbles per second, while the second one only computes
.020 MegaFrumbles per second; hence the speed of the first one is
(.025-.020)/.020 = 25% faster than the speed of the second one.
Translation Inadequacy due to the FreeVars Trip-Up
Actually, it's just as well that I waited until today to report to you,
since the **major factor** in the timings compared so far is the old
"FreeVars Trip-Up", and anyway Boyer's latest modification is more
appropriate for benchmarking, period. I have quite a few interesting
timings to report (and a few remaining mysteries regarding your
machine), but indeed the major discrepancy between your timings
and mine was that the version of IREWRITE we had at Parc is the one
that Larry had "diddled" as per his earlier note.
On your machine, I saw a 50% speedup due to better treatment of the
free variable TEMP-TEMP. (My runs of your original version of
IREWRITE compared with Larry's "diddled" version).
On several machines here, I compared Larry's "diddled" version with
Boyer's new version, and observed about a 9% speed-up of the latter
over the former. Converting TEMP-TEMP from a local variable to a
GLOBALVAR should cause a slowdown in the 1% range (a GLOBALVAR
usage may take time for a GC-hash-table operation, but a LOCALVAR
usage takes time only for pushing/popping the stack) but Boyer changed
several other bottlenecks and the speed increases therefrom more than
compensated for the loss of the local variable (SASSOC ==> FASSOC,
and the placement of important properties at the beginning of the proplist ?)
In any case, this benchmark exhibits a factor of two improvement by
removing what I'm calling the "FreeVars Trip-Up".
This point can't be overstressed: that Interlisp-D is a deep-bound
implementation, whereas MacLisp and current Interlisp-10 are shallow-
bound (Interlisp-10 was first deep-bound, then later shallow-bound),
and that the questionable practice of using free variables for local
temporaries costs little when they are shallow-bound, but could
cost arbitrarily large when deep-bound. I say, "questionable" since a
program with such temporaries is semantically the same regardless of
whether they are GLOBAL, SPECIAL, or local; furthermore, the
general direction of "structured programming" is to avoid free variables
at all costs, and to bind temporaries as syntactically "low" as possible.
The *default* declaration for variables in Interlisp is SPECVARS, for
consistency with the way the interpreter is written, and thus the default
compilation of a free variable will cause a stack scan (slow) rather than a
reference to the global value cell (fast). So one does have to take *some*
action to override the default case when transporting such a program.
A recent Symbolics advertising flyer makes a "comparison" of an Interlisp
program running on the Dolphin and on the LM-2. It wasn't so much
a comparison between Interlisp-D/Dolphin with ZetaLisp/CADR as a
documentation of someone's failure to add the appropriate GLOBALVARS
delcarations. I heard (admittedly, hearsay) that the ISI guy whose program
was under test made the additional declaration himself, and the Dolphin
performance "improved by 67%". [One also wonders how the "comparison"
would have fared had the LISPMachine garbage collector been operable;
a large percentage of the Dolphin time was spent in GC, which helps keep
the working-set small, and also allows you to continue running *after*
the benchmark has finished running.]
"Ineffable" Factors Tending to make timing runs Un-Reproducible
As Larry's note indicated, there is a hidden problem with swap time in
the Interlisp-D of today -- an "ineffable" amount of it is being charged
to CPU time rather than the reported Swap time. The data below seem
to indicate anywhere from 5% to 20% of reported CPU time is really swap
time, when there is indeed swapping going on.
You're quite right, however, that swapping-time is a small factor in this
benchmark; although there consistently seemed to be more of it on your
machine than mine (about 8%, depending on method of interpretation of
the "ineffable" considerations herein mentioned). That's mystery number 1,
since both your machine and mine have the same amount of real memory,
namely about 1.15 Megabyte. The proper setting of RECLAIMMIN keeps
both our Dolphins from "going over the knee" on this benchmark, although
a large setting for my Dolphin caused the CPU time to go up by 50%
and the Swap time to go up from essentially 0 to almost 600 seconds. A
Dorado, with 2 Megabytes and a faster swapping-disk, didn't "go over the
knee" even with the extreme high setting of RECLAIMMIN.
During the first run of TEST, additional pages are added to LIST space,
and the cost of doing this is difficult to estimate accurately in the current
setup. The STATS I ran on the Dorado showed nearly 20% of the
total first-run time given to this activity, but this is inflated by the
fact that the run had to be terminated abnormally (ran out of DSK space
for keeping statistics); this "ineffable" time would concentrate in the
early part of the run. But a 5%-10% slowdown due to this facter seems
indicated in general (my "educated guess" from mulling over the data).
There is a certain oddity about the reference-count GC scheme in that
a call to RECLAIM may not necessarily recover all reclaimable space.
Without going into the details of this oddity, I merely observed that
between TEST runs, it was necessary to do several iterations of
(RECLAIM) before the time spent therein settled down to a typical low
value [indicating that most if not all reclaimables were in fact reclaimed].
This is why I've indicated a "mode" run -- namely the timings that are
most often seen after the initial swap-in, initial swell-up of LIST space,
and "cleanness" of the reclaimable space are accounted for. But I must
confess, that I hadn't discovered all of these things initially, so there is
a little uncertainty about the "mode" timings done on July 2.
PUP Activity -- Ephemeral as well as Ineffable
Mystery number 2 is why the "diddled" TEST run on your machine has
a "mode" of 210 CPU seconds as opposed to about 143 CPU seconds on a
comparably-clocked machine here running the current CONBRIO release.
(This was my measurement for the "diddled" version -- you reported 278
for the original version and I recorded 299. for the original version -- but
the "diddled" version is *exactly* the same file I had at PARC, in the same
release of Lisp).
It's almost as if you had some large overhead activity going on all the time,
such as snarfing up random PUPs and throwing them away. Pup activity
could be a highly-variable thing, and could account for large timing
differences between say Friday afternoon and Thursday morning.
Unfortunately, its also something that is not easily controlled by a user
doing timings, since it depends the PUP activity of others users of the
same ethernet. Currently, time spent in Interlisp-D "dropping" non-
intended PUPs is not visible in the timings statistics (it would merely
bloat reported CPU time). PUP activity could be monitored by another
Dolphin running EtherWatch while you are running timings on yours.
[A simple way of temporarily turning off PUP activity might help
filter out this as a source of variability; are you interested in trying?]
What the Faster Clock on buys
My Dolphin is indeed faster than many others, because it has a clock
crystal running at 44.5 MegaHertz. The Dolphin was originally intended
to run at 50MHz, but due to a larger-than-expected variability in the
components (chips, etc) the production models are currently pegged at
40MHz. Machines with a 44.5MHz clock have a speed increase of about 12% to
16%. The reason why this isn't merely 10% is that there is a "buffering"
action of the constant-time overhead required for maintaining the display
and sampling the keyboard; thus a faster machine spends proportionately
less of its time in these constant overhead tasks. Of course, 50MHz clocks
would result in even more performance improvement.
What DISPLAYDOWN buys
I thought that you had run with DISPLAYDOWN during the compute-
bound TEST; so I ran this way on my runs, except for those intended
to gather data which would correlate the effect of DISPLAYDOWN.
It makes sense to do so on *compute-bound* tasks, since an average
speed increase of 41% to 45% is thereby obtained.
As expected, the display off means more to CPU time on a 40MHz
machine than to that on a 44.5MHz one -- 43% as opposed to only 36%.
GC timings are so variable that I factored them out for these percentages.
[I don't think one would see anything like this gain if the keyboard
sampling mentioned above were similarly shut off; Dorado STATS point
to maybe 6% possible, but even this overhead cost may go down as more
software is developed. As a side comment, display maintenance is not
a significant factor in the Dorado or in the DandeLion.]
What you can Expect for Dolphin Speed Increases Soon
The WIND version of the software will likely be released later this
year, and the data herein indicate a minimum of about 10% overall
increase in speed; other preliminary measures suggest a speed-up of
15% to 20%. Faster hardware may be in the works, but I'm not the one
to comment in any offical way about this. Maybe when we get some
more benchmarks (such as Dick Gabriel is pushing for), we'll do them
on the latest Dolphins.
Just for the record, I'd like to include some timings given me by Larry,
which were done on the Dolphin of one year ago (the "diddled" version
of the problem):
Swap time = 30secs
GC time = 175secs
CPU time = 750secs
Elapsed = 950secs
So today's "vanilla" times are 5.6 times faster than last years, and on my
44.5Mhz machine running WIND I see a speed-up of a factor of 7.
A factor of 7!
Bill van Melle suggests that these speed-ups are due mainly to improvements
in function call and CONS, and that's precisely what the Boyer-Moore
IREWRITE benchmark tests. I really don't think anything quite that dramatic is
on the horizon for the *overall* Dolphin performance, but *selected areas*
which we have targeted for more devolpment could show stellar improvement.
(such as putting floating-point into microcode).
Hope to see you at AAAI.
_________________________________________________
The Raw Data
Machines: GSN (Gordon Novak's), JONL (mine), SYBAL (John Sybalsky's)
[GSN and SYBAL have 40MHz, JONL has 44.5MHz]
Finisterra (the only Dorado included)
Program: OB (Old Boyer code, without declarations)
NB (New Boyer code, with GLOBALVARS for free temps)
Diddled (Larry Masinter's reworking using local lambda
binding for temporaries)
Version: CB (current release CONBRIO), WD (WIND system)
Options: DD (display "down", or off), DU (display "up")
1st (first run), nth ("mode", or most frequently observed after first)
All measurements in seconds. Timings on SYBAL,NB,CB,DD were also
reproduced quite closely on Larry Masinter's machine, and on Stu Card's.
Display Up vs. Display Down times
-----------------------------------------------------------------
Swap 3.6 GSN | Swap 3.0 GSN July 2
GC 66.4 OB | GC 49. OB
CPU 415. CB,DU,nth | CPU 299. CB,DD,nth
Swap 33.1 GSN | Swap 5.7 GSN July 2
GC 70.0 diddled | GC 50.9 diddled
CPU 305. CB,DU,1st | CPU 210. CB,DD,nth
Swap 0.5 JONL | Swap - JONL July 2
GC 60. diddled | GC 30.2 diddled
CPU 158. WD,DU,nth | CPU 116. WD,DD,nth
Swap - SYBAL | Swap - SYBAL July 7
GC 56. diddled | GC 39.6 diddled
CPU 204. CB,DU,nth | CPU 143. CB,DD,nth
First run vs. nth ("mode") run; Display Down
-----------------------------------------------------------------
Swap 2. JONL | Swap - JONL July 7
GC 26.7 NB | GC 31.6 NB
CPU 142. CB,DD,1st | CPU 117. CB,DD,nth
Swap .2 JONL | Swap - JONL July 7
GC 24.9 NB | GC 28.2 NB
CPU 119. WD,DD,1st | CPU 107. WD,DD,nth
Swap 9.8 SYBAL | Swap - SYBAL July 7
GC 31. NB | GC 35. NB
CPU 140. CB,DD,1st | CPU 132. CB,DD,nth
Swap .14 SYBAL | Swap - SYBAL July 7
GC 20.6 NB | GC 31.7 NB
CPU 133. WD,DD,1st | CPU 119. WD,DD,nth
Swap .1 SYBAL | Swap - SYBAL July 7
GC 33.2 diddled | GC 35. diddled
CPU 150. WD,DD,1st | CPU 130. WD,DD,nth
Dorado time
-----------------------------------------------------------------
Swap ? Finisterra | Swap - Finisterra July 2
GC 11.4 diddled | GC 17. diddled
CPU 25.6 WD,1st | CPU 22.7 WD,nth
The STATS file mentioned for Dorado analysis is on the PHYLUM
file server at PARC, file <JONL>TEST.PRINTOUT. Since it's a
lengthy account of an incomplete run, I didn't reproduce it here.
Mail-from: ARPANET site SU-SCORE rcvd at 8-Jul-82 1245-CDT
Date: 8 Jul 1982 1043-PDT
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
To: Masinter at PARC-MAXC, CL.BOYER at UTEXAS-20
cc: JonL at PARC-MAXC
In-Reply-To: Your message of 7-Jul-82 1812-PDT
Date: Thursday, 8 July 1982 12:43-CDT
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
To: Masinter at PARC-MAXC, CL.BOYER
cc: JonL at PARC-MAXC
I reran the test as Larry did, with similar results (included below).
My problem was that I used TCOMPL instead of BCOMPL. I recall being
told by someone that the Dolphin didn't block-compile like Interlisp-10,
so that BCOMPL and TCOMPL did the same thing. Obviously that isn't true;
I should have been more careful. I apologize for raising a ruckus over
a silly mistake; at least I'm glad that the results will be fair to the
Dolphin crowd.
DISPLAYDOWN, as used in Larry's test, totally turns off the display for
the duration. I haven't used it myself, but I understand that it can
get one into funny problemsif e.g. there are errors in the execution
of the program with the display off; I don't know if most users would
find it acceptable to run in this mode.
NIL
Mail-from: ARPANET site PARC-MAXC rcvd at 13-Jul-82 0217-CDT
From: JonL at PARC-MAXC
To: CL.BOYER
cc: JonL at PARC-MAXC
Re: Timings Table for IREWRITE benchmark
Yes, the SYBAL,NB,CB,DD is an appropriate time for the current "vanilla"
Dolphin; but the Dorado timing I reported in the previous note can't be
strictly compared with the others since it was running the "diddled" test
rather than the NewBoyer (NB) test, and was in the WIND release rather
than CONBRIO. [As it happens, the "diddling" had somewhat of a misfeature
in it, which is why I mentioned that NB is a much better benchmark anyway].
Dorado Frontenac, NewBoyer.benchmark(NB),systemCONBRIO(CB)
DisplayDown (DD) times for "mode" (nth) run:
GC = 10.9
CPU = 17.6
DisplayUp (DU) times for "mode" (nth) run:
GC = 11.8
CPU = 19.2
DisplayDown (DD) times for "FirstRun" (1st) run:
Swap = .027
GC = 10.5
CPU = 17.4
It's not clear to me why the "FirstRun" time was faster in these trials -- chalk
it up to "noise", or maybe to the benefits of larger-memory/faster-disk?
∨
←LOAD(IREWRITE.DCOM)
compiled on 8-JUL-82 09:54:44
FILE CREATED 5-Jul-82 12:52:49
IREWRITECOMS
{DSK}IREWRITE.DCOM;2
←(DISPLAYDOWN (TIMEALL (SETUP)))
Elapsed Time = .755 seconds
SWAP time = .582 seconds
CPU Time = .173 seconds
PAGEFAULTS = 12
LISTP
224
T
←(DISPLAYDOWN '(TIMEALL (TEST)))
Elapsed Time = 175.0 seconds
SWAP time = 6.63 seconds
GC time = 31.5 seconds
CPU Time = 137.0 seconds
PAGEFAULTS = 610
SWAPWRITES = 157
FIXP LISTP
311 226469
(T 168388 31471)
←REDO
Elapsed Time = 183.0 seconds
SWAP time = .494 seconds
GC time = 48.7 seconds
CPU Time = 134.0 seconds
PAGEFAULTS = 21
FIXP LISTP
375 226469
(T 182913 48703)
←REDO
Elapsed Time = 188.0 seconds
SWAP time = .078 seconds
GC time = 52.3 seconds
CPU Time = 136.0 seconds
PAGEFAULTS = 2
FIXP LISTP
419 226469
(T 188209 52257)
←REDO
Elapsed Time = 188.0 seconds
SWAP time = .015 seconds
GC time = 51.2 seconds
CPU Time = 137.0 seconds
PAGEFAULTS = 14
FIXP LISTP
401 226469
(T 187906 51188)
←TIMEALL((TEST))
Elapsed Time = 271.0 seconds
SWAP time = .059 seconds
GC time = 75.3 seconds
CPU Time = 195.0 seconds
PAGEFAULTS = 1
FIXP LISTP
420 226469
(T 270715 75315)
←TIMEALL((TEST))
Elapsed Time = 267.0 seconds
SWAP time = .006 seconds
GC time = 73.2 seconds
CPU Time = 194.0 seconds
PAGEFAULTS = 6
FIXP LISTP
402 226469
(T 267145 73153)
←TIMEALL((TEST))
Elapsed Time = 266.0 seconds
GC time = 72.6 seconds
CPU Time = 194.0 seconds
FIXP LISTP
402 226469
(T 266215 72623)
←DRIBBLE]
∨
The INTERLISP VAX test
Mail-from: ARPANET site USC-ISIB rcvd at 23-Jul-82 1108-CDT
Date: 23 Jul 1982 0907-PDT
Sender: RBATES at USC-ISIB
Subject: Re: lisp comparison.
From: Raymond Bates <RBATES at ISIB>
To: CL.BOYER at UTEXAS-20
Cc: CMP.GOOD at UTEXAS-20, ddyer at USC-ISIB, lynch at USC-ISIB,
Cc: Novak at SUMEX-AIM
Message-ID: <[USC-ISIB]23-Jul-82 09:07:07.RBATES>
In-Reply-To: Your message of Thursday, 22 July 1982 13:12-CDT
*** EOOH ***
Date: Friday, 23 July 1982 11:07-CDT
From: Raymond Bates <RBATES at ISIB>
Sender: RBATES at USC-ISIB
To: CL.BOYER
cc: CMP.GOOD, ddyer at USC-ISIB, lynch at USC-ISIB, Novak at SUMEX-AIM
Re: lisp comparison.
Here is the DRIBBLE file of a long run:
NIL
4←(GCGAG NIL]
40
5←LOAD(IREWRITE.v]
compiled on 22-JUL-82 09:22:17
File Created: 5-Jul-82 12:52:49
% warning! this file possibly incompatible!
Compiled by version 3.0 but current version is 2.1
IREWRITECOMS
/lisp/rbates/lisp/IREWRITE.v;2
6←(SETUP]
T
7←(FOR I FROM 1 TO 20 DO (PRINT (TEST ]
(T 76048 0)
(T 76464 0)
(T 76496 0)
(T 76272 0)
(T 89072 4784)
(T 80992 0)
(T 81840 0)
(T 81600 0)
(T 90512 4752)
(T 81904 0)
(T 82032 0)
(T 81248 0)
(T 90512 5456)
(T 80768 0)
(T 80800 0)
(T 80656 0)
(T 91424 5456)
(T 82112 0)
(T 82384 0)
(T 82432 0)
NIL
8←(DRIBBLE]
You many wonder why the cpu time has an extra 10 seconds each
time the system does a gc. The reason is that the system has to
re-hash all the hash array after the gc and time is being charge
to the computation time and not gc time (we will fix that). This
test was done on our 780. Any thing else you would like to see
or known?
/Ray
∨
;;; SAIL
(fasload boyer)
(timit)
Timing performed on Wednesday 09/15/82 at 10:50:58.
Cpu Time = 7.635
Elapsed Time = 726.53333
Wholine Time = 241.866667
GC Time = 120.472
Load Average Before = 6.1742424
Load Average After = 2.85985446
Average Load Average = 4.5170484
NIL
Timing performed on Wednesday 09/15/82 at 11:03:27.
Cpu Time = 7.49
Elapsed Time = 65.0
Wholine Time = 36.4166665
GC Time = 12.669
Load Average Before = 2.54934967
Load Average After = 2.2733817
Average Load Average = 2.4113657
NIL
Timing performed on Wednesday 09/15/82 at 11:04:44.
Cpu Time = 7.509
Elapsed Time = 59.3166666
Wholine Time = 32.866667
GC Time = 11.513
Load Average Before = 2.17366004
Load Average After = 2.06962526
Average Load Average = 2.12164265
NIL
;;; SAIL (FIXSW T)
(fasload boyer)
(timit)
Timing performed on Wednesday 09/15/82 at 11:06:16.
Cpu Time = 7.629
Elapsed Time = 1076.21666
Wholine Time = 229.366667
GC Time = 120.4
Load Average Before = 1.81269705
Load Average After = 8.4301555
Average Load Average = 5.1214263
NIL
Timing performed on Wednesday 09/15/82 at 11:24:17.
Cpu Time = 7.494
Elapsed Time = 86.016666
Wholine Time = 36.733333
GC Time = 12.692
Load Average Before = 8.2354884
Load Average After = 5.64889336
Average Load Average = 6.9421909
NIL
Timing performed on Wednesday 09/15/82 at 11:25:45.
Cpu Time = 7.484
Elapsed Time = 82.3
Wholine Time = 33.983333
GC Time = 11.519
Load Average Before = 5.58177483
Load Average After = 4.12152493
Average Load Average = 4.8516499
NIL